Nuprl Lemma : same-thread_weakening
11,40
postcript
pdf
es
:ES,
p
:(E
(E + Top)).
causal-predecessor(
es
;
p
)
(
e
,
e'
:E. (
e
=
e'
)
same-thread(
es
;
p
;
e
;
e'
))
latex
Definitions
x
,
y
.
t
(
x
;
y
)
,
True
,
T
,
same-thread(
es
;
p
;
e
;
e'
)
,
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
x
(
s1
,
s2
)
Lemmas
causal-pred-wellfounded
,
p-graph
wf2
,
strongwellfounded
wf
,
squash
wf
,
final-iterate
wf
,
event
system
wf
,
top
wf
,
causal-predecessor
wf
,
es-E
wf
origin
es:ES, p:(E
(E + Top)).
(e, e':E. (e = e') same-thread(es;p;e;e')) es:ES, p:(E(E + Top)).
(e, e':E. (e = e') same-thread(es;p;e;e')) 
x,y. t(x;y)
T
T Qx:A. B(x)